Search Results

Documents authored by Kwiatkowska, Marta Z.

Found 2 Possible Name Variants:

Kwiatkowska, Marta Z.

Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2019.1
Safety Verification for Deep Neural Networks with Provable Guarantees (Invited Paper)

Authors: Marta Z. Kwiatkowska

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Computing systems are becoming ever more complex, increasingly often incorporating deep learning components. Since deep learning is unstable with respect to adversarial perturbations, there is a need for rigorous software development methodologies that encompass machine learning. This paper describes progress with developing automated verification techniques for deep neural networks to ensure safety and robustness of their decisions with respect to input perturbations. This includes novel algorithms based on feature-guided search, games, global optimisation and Bayesian methods.
Cite as

Marta Z. Kwiatkowska. Safety Verification for Deep Neural Networks with Provable Guarantees (Invited Paper). In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kwiatkowska:LIPIcs.CONCUR.2019.1,
  author =	{Kwiatkowska, Marta Z.},
  title =	{{Safety Verification for Deep Neural Networks with Provable Guarantees}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{1:1--1:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.1},
  URN =		{urn:nbn:de:0030-drops-109036},
  doi =		{10.4230/LIPIcs.CONCUR.2019.1},
  annote =	{Keywords: Neural networks, robustness, formal verification, Bayesian neural networks}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICALP.2016.4
Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice (Invited Talk)

Authors: Marta Z. Kwiatkowska

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
Probabilistic model checking is an automatic procedure for establishing if a desired property holds in a probabilistic model, aimed at verifying quantitative probabilistic specifications such as the probability of a critical failure occurring or expected time to termination. Much progress has been made in recent years in algorithms, tools and applications of probabilistic model checking, as exemplified by the probabilistic model checker PRISM (http://www.prismmodelchecker.org). However, the unstoppable rise of autonomous systems, from robotic assistants to self-driving cars, is placing greater and greater demands on quantitative modelling and verification technologies. To address the challenges of autonomy we need to consider collaborative, competitive and adversarial behaviour, which is naturally modelled using game-theoretic abstractions, enhanced with stochasticity arising from randomisation and uncertainty. This paper gives an overview of quantitative verification and strategy synthesis techniques developed for turn-based stochastic multi-player games, summarising recent advances concerning multi-objective properties and compositional strategy synthesis. The techniques have been implemented in the PRISM-games model checker built as an extension of PRISM.
Cite as

Marta Z. Kwiatkowska. Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice (Invited Talk). In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{kwiatkowska:LIPIcs.ICALP.2016.4,
  author =	{Kwiatkowska, Marta Z.},
  title =	{{Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{4:1--4:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.4},
  URN =		{urn:nbn:de:0030-drops-62285},
  doi =		{10.4230/LIPIcs.ICALP.2016.4},
  annote =	{Keywords: Quantitative verification, Stochastic games, Temporal logic, Model checking, Strategy synthesis}
}

Kwiatkowska, Marta

Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2024.5
Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms (Invited Talk)

Authors: Marta Kwiatkowska

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
Strategic reasoning is essential to ensure stable multi-agent coordination in complex environments, as it enables synthesis of optimal (or near-optimal) agent strategies and equilibria that guarantee expected outcomes, even in adversarial scenarios. Partially-observable stochastic games (POSGs) are a natural model for real-world settings involving multiple agents, uncertainty and partial information, but lack practical algorithms for computing or approximating optimal values and strategies. Recently, progress has been made for one-sided POSGs, a subclass of two-agent, zero-sum POSGs where only one agent has partial information while the other agent is assumed to have full knowledge of the state, with heuristic search value iteration (HSVI) proposed for computing approximately optimal values and strategies in one-sided POSGs [Horák et al., 2023]. This model is well suited to safety-critical applications, when making worst-case assumptions about one agent; examples include the attacker in a security application, modelled, e.g., as a patrolling or pursuit-evasion game. However, many realistic autonomous coordination scenarios involve agents perceiving continuous environments using data-driven observation functions, typically implemented as neural networks (NNs). Examples include autonomous vehicles using NNs to perform object recognition or to estimate pedestrian intention, or NN-enabled vision in an airborne pursuit-evasion scenario. Such perception mechanisms bring new challenges, notably continuous environments, which are inherently tied to NN-enabled perception because of standard training regimes. This means that naive discretisation is difficult, since decision boundaries obtained for data-driven perception are typically irregular and can be misaligned with gridding schemes for discretisation, affecting the precision of the computed strategies. This invited paper will discuss progress with developing a model class and algorithms for one-sided POSGs with neural perception mechanisms [R. Yan et al., 2022; Yan et al., 2023] that work directly with their continuous state space. Building on continuous-state POMDPs with NN perception mechanisms [Yan et al., 2023], where the key idea is that ReLU neural network classifiers induce a finite decomposition of the continuous environment into polyhedra for each classification label, a piecewise constant representation for the value, reward and perception functions is developed that forms the basis for a variant of HSVI, a point-based solution method that computes a lower and upper bound on the value function from a given belief to compute an (approximately) optimal strategy. We extend these ideas from the single-agent (POMDP) setting [Yan et al., 2023] to zero-sum POSGs. In the game setting, this involves solving a normal form game at each stage and iteration, and goes significantly beyond HSVI for finite POSGs [Horák et al., 2023].
Cite as

Marta Kwiatkowska. Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kwiatkowska:LIPIcs.CSL.2024.5,
  author =	{Kwiatkowska, Marta},
  title =	{{Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{5:1--5:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.5},
  URN =		{urn:nbn:de:0030-drops-196471},
  doi =		{10.4230/LIPIcs.CSL.2024.5},
  annote =	{Keywords: Stochastic games, neural networks, formal verification, strategy synthesis}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2023.1
CONCUR Test-Of-Time Award 2023 (Invited Paper)

Authors: Bengt Jonsson, Marta Kwiatkowska, and Igor Walukiewicz

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
This short article recaps the purpose of the CONCUR Test-of-Time Award and presents the paper that received the Award in 2023.
Cite as

Bengt Jonsson, Marta Kwiatkowska, and Igor Walukiewicz. CONCUR Test-Of-Time Award 2023 (Invited Paper). In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jonsson_et_al:LIPIcs.CONCUR.2023.1,
  author =	{Jonsson, Bengt and Kwiatkowska, Marta and Walukiewicz, Igor},
  title =	{{CONCUR Test-Of-Time Award 2023}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.1},
  URN =		{urn:nbn:de:0030-drops-189953},
  doi =		{10.4230/LIPIcs.CONCUR.2023.1},
  annote =	{Keywords: CONCUR Test-of-Time Award}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2022.4
Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk)

Authors: Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos, and Rui Yan

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
Game-theoretic concepts have been extensively studied in economics to provide insight into competitive behaviour and strategic decision making. As computing systems increasingly involve concurrently acting autonomous agents, game-theoretic approaches are becoming widespread in computer science as a faithful modelling abstraction. These techniques can be used to reason about the competitive or collaborative behaviour of multiple rational agents with distinct goals or objectives. This paper provides an overview of recent advances in developing a modelling, verification and strategy synthesis framework for concurrent stochastic games implemented in the probabilistic model checker PRISM-games. This is based on a temporal logic that supports finite- and infinite-horizon temporal properties in both a zero-sum and nonzero-sum setting, the latter using Nash and correlated equilibria with respect to two optimality criteria, social welfare and social fairness. We summarise the key concepts, logics and algorithms and the currently available tool support. Future challenges and recent progress in adapting the framework and algorithmic solutions to continuous environments and neural networks are also outlined.
Cite as

Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos, and Rui Yan. Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk). In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kwiatkowska_et_al:LIPIcs.MFCS.2022.4,
  author =	{Kwiatkowska, Marta and Norman, Gethin and Parker, David and Santos, Gabriel and Yan, Rui},
  title =	{{Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{4:1--4:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.4},
  URN =		{urn:nbn:de:0030-drops-168026},
  doi =		{10.4230/LIPIcs.MFCS.2022.4},
  annote =	{Keywords: Probabilistic model checking, stochastic games, equilibria}
}
Document
DOI: 10.4230/DagRep.5.11.151
Approximate and Probabilistic Computing: Design, Coding, Verification (Dagstuhl Seminar 15491)

Authors: Antonio Filieri, Marta Kwiatkowska, Sasa Misailovic, and Todd Mytkowicz

Published in: Dagstuhl Reports, Volume 5, Issue 11 (2016)

Abstract
Computing has entered the era of approximation, in which hardware and software generate and reason about estimates. Navigation applications turn maps and location estimates from hardware GPS sensors into driving directions; speech recognition turns an analog signal into a likely sentence; search turns queries into information; network protocols deliver unreliable messages; and recent advances promise that approximate hardware and software will trade result quality for energy efficiency. Millions of people already use software which computes with and reasons about approximate/probabilistic data daily. These complex systems require sophisticated algorithms to deliver accurate answers quickly, at scale, and with energy efficiency, and approximation is often the only way to meet these competing goals. Despite their ubiquity, economic significance, and societal impact, building such applications is difficult and requires expertise across the system stack, in addition to statistics and application-specific domain knowledge. Non-expert developers need tools and expertise to help them design, code, and verify these complex systems. The aim of this seminar was to bring together academic and industrial researchers from the areas of probabilistic model checking, quantitative software analysis, probabilistic programming, and approximate computing to share their recent progress, identify challenges in computing with estimates, and foster collaboration with the goal of helping non-expert developers design, code, and verify modern approximate and probabilistic systems.
Cite as

Antonio Filieri, Marta Kwiatkowska, Sasa Misailovic, and Todd Mytkowicz. Approximate and Probabilistic Computing: Design, Coding, Verification (Dagstuhl Seminar 15491). In Dagstuhl Reports, Volume 5, Issue 11, pp. 151-179, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{filieri_et_al:DagRep.5.11.151,
  author =	{Filieri, Antonio and Kwiatkowska, Marta and Misailovic, Sasa and Mytkowicz, Todd},
  title =	{{Approximate and Probabilistic Computing: Design, Coding, Verification (Dagstuhl Seminar 15491)}},
  pages =	{151--179},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{11},
  editor =	{Filieri, Antonio and Kwiatkowska, Marta and Misailovic, Sasa and Mytkowicz, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.11.151},
  URN =		{urn:nbn:de:0030-drops-58008},
  doi =		{10.4230/DagRep.5.11.151},
  annote =	{Keywords: approximation, model checking, performance, probability, program analysis, systems, verification}
}
Document
Invited Paper
DOI: 10.4230/OASIcs.SynCoP.2015.16
Parameter synthesis for probabilistic real-time systems (Invited Paper)

Authors: Marta Kwiatkowska

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
The parameter synthesis problem aims to find parameter valuations that guarantee that a given objective is satisfied for a parametric model. Applications range from automated model repair to optimisation. This lecture will focus on models with probability and real-time and give an overview of recent results concerning parameter synthesis from quantitative temporal logic objectives. Existing algorithmic approaches and experimental results will be discussed, and future research challenges outlined.
Cite as

Marta Kwiatkowska. Parameter synthesis for probabilistic real-time systems (Invited Paper). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, p. 16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kwiatkowska:OASIcs.SynCoP.2015.16,
  author =	{Kwiatkowska, Marta},
  title =	{{Parameter synthesis for probabilistic real-time systems}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{16--16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.16},
  URN =		{urn:nbn:de:0030-drops-56062},
  doi =		{10.4230/OASIcs.SynCoP.2015.16},
  annote =	{Keywords: Quantitative verification, Timed automata, Parameter synthesis}
}
Document
DOI: 10.4230/DagRep.5.1.164
Model-driven Algorithms and Architectures for Self-Aware Computing Systems (Dagstuhl Seminar 15041)

Authors: Samuel Kounev, Xiaoyun Zhu, Jeffrey O. Kephart, and Marta Kwiatkowska

Published in: Dagstuhl Reports, Volume 5, Issue 1 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15041 "Model-driven Algorithms and Architectures for Self-Aware Computing Systems". The design of self-aware computing systems calls for an integrated interdisciplinary approach building on results from multiple areas of computer science and engineering, including software and systems engineering, systems modeling, simulation and analysis, autonomic and organic computing, machine learning and artificial intelligence, data center resource management, and so on. The Dagstuhl Seminar 15041 served as a platform to raise the awareness about the relevant research efforts in the respective research communities as well as existing synergies that can be exploited to advance the state-of-the-art, formulate a new research agenda that takes a broader view on the problem following an integrated and interdisciplinary approach, and establish collaborations between academia and industry.
Cite as

Samuel Kounev, Xiaoyun Zhu, Jeffrey O. Kephart, and Marta Kwiatkowska. Model-driven Algorithms and Architectures for Self-Aware Computing Systems (Dagstuhl Seminar 15041). In Dagstuhl Reports, Volume 5, Issue 1, pp. 164-196, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{kounev_et_al:DagRep.5.1.164,
  author =	{Kounev, Samuel and Zhu, Xiaoyun and Kephart, Jeffrey O. and Kwiatkowska, Marta},
  title =	{{Model-driven Algorithms and Architectures for Self-Aware Computing Systems (Dagstuhl Seminar 15041)}},
  pages =	{164--196},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{1},
  editor =	{Kounev, Samuel and Zhu, Xiaoyun and Kephart, Jeffrey O. and Kwiatkowska, Marta},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.1.164},
  URN =		{urn:nbn:de:0030-drops-50385},
  doi =		{10.4230/DagRep.5.1.164},
  annote =	{Keywords: autonomic systems, self-adaptive, self-managing, model-driven, architecture-based, systems management, machine learning, feedback-based design}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.MCPS.2014
OASIcs, Volume 36, MCPS'14, Complete Volume

Authors: Volker Turau, Marta Kwiatkowska, Rahul Mangharam, and Christoph Weyer

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)

Abstract
OASIcs, Volume 36, MCPS'14, Complete Volume
Cite as

5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Proceedings{turau_et_al:OASIcs.MCPS.2014,
  title =	{{OASIcs, Volume 36, MCPS'14, Complete Volume}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014},
  URN =		{urn:nbn:de:0030-drops-45403},
  doi =		{10.4230/OASIcs.MCPS.2014},
  annote =	{Keywords: Conference proceedings}
}
Document
Front Matter
DOI: 10.4230/OASIcs.MCPS.2014.i
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Volker Turau, Marta Kwiatkowska, Rahul Mangharam, and Christoph Weyer

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)

Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as

5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. i-x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{turau_et_al:OASIcs.MCPS.2014.i,
  author =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  pages =	{i--x},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014.i},
  URN =		{urn:nbn:de:0030-drops-45174},
  doi =		{10.4230/OASIcs.MCPS.2014.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
DOI: 10.4230/OASIcs.MCPS.2014.137
Automated Verification of Quantitative Properties of Cardiac Pacemaker Software

Authors: Marta Kwiatkowska and Alexandru Mereacre

Published in: OASIcs, Volume 36, 5th Workshop on Medical Cyber-Physical Systems (2014)

Abstract
This poster paper reports on a model-based framework for software quality assurance for cardiac pacemakers developed in Simulink and described in [Chen/Diciolla/Kwiatkowska/Mereacre - Information&Computation, 2013]. A novel hybrid heart model is proposed that is suitable for quantitative verification of pacemakers. The heart model is formulated at the level of cardiac cells, can be adapted to patient data, and incorporates stochasticity. We validate the model by demonstrating that its composition with a pacemaker model can be used to check safety properties by means of approximate probabilistic verification.
Cite as

Marta Kwiatkowska and Alexandru Mereacre. Automated Verification of Quantitative Properties of Cardiac Pacemaker Software. In 5th Workshop on Medical Cyber-Physical Systems. Open Access Series in Informatics (OASIcs), Volume 36, pp. 137-140, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{kwiatkowska_et_al:OASIcs.MCPS.2014.137,
  author =	{Kwiatkowska, Marta and Mereacre, Alexandru},
  title =	{{Automated Verification of Quantitative Properties of Cardiac Pacemaker Software}},
  booktitle =	{5th Workshop on Medical Cyber-Physical Systems},
  pages =	{137--140},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-66-8},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{36},
  editor =	{Turau, Volker and Kwiatkowska, Marta and Mangharam, Rahul and Weyer, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.MCPS.2014.137},
  URN =		{urn:nbn:de:0030-drops-45317},
  doi =		{10.4230/OASIcs.MCPS.2014.137},
  annote =	{Keywords: Pacemakers, Verification, Simulink}
}
Document
DOI: 10.4230/DagSemProc.10051.1
10051 Abstracts Collection – Quantitative and Qualitative Analysis of Network Protocols

Authors: Bengt Jonsson, Jörg Kreiker, and Marta Kwiatkowska

Published in: Dagstuhl Seminar Proceedings, Volume 10051, Quantitative and Qualitative Analysis of Network Protocols (2010)

Abstract
From Jan 31, 2010 to Feb 5, 2010, the Dagstuhl Seminar 10051 ``Quantitative and Qualitative Analysis of Network Protocols '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Bengt Jonsson, Jörg Kreiker, and Marta Kwiatkowska. 10051 Abstracts Collection – Quantitative and Qualitative Analysis of Network Protocols. In Quantitative and Qualitative Analysis of Network Protocols. Dagstuhl Seminar Proceedings, Volume 10051, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{jonsson_et_al:DagSemProc.10051.1,
  author =	{Jonsson, Bengt and Kreiker, J\"{o}rg and Kwiatkowska, Marta},
  title =	{{10051 Abstracts Collection – Quantitative and Qualitative Analysis of Network Protocols}},
  booktitle =	{Quantitative and Qualitative Analysis of Network Protocols},
  pages =	{1--14},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10051},
  editor =	{Bengt Jonsson and J\"{o}rg Kreiker and Marta Kwiatkowska},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10051.1},
  URN =		{urn:nbn:de:0030-drops-25186},
  doi =		{10.4230/DagSemProc.10051.1},
  annote =	{Keywords: Network protocols, verification, static analysis, quantitative modeling and model checking, graph transformation, process calculi}
}
Document
DOI: 10.4230/DagSemProc.10051.2
10051 Executive Summary – Quantitative and Qualitative Analysis of Network Protocols

Authors: Bengt Jonsson, Jörg Kreiker, and Marta Kwiatkowska

Published in: Dagstuhl Seminar Proceedings, Volume 10051, Quantitative and Qualitative Analysis of Network Protocols (2010)

Abstract
This is the executive summary for the seminar Quantitative and Qualitative Analysis of Network Protocols held from Jan 31, 2010 to Feb 5, 2010.
Cite as

Bengt Jonsson, Jörg Kreiker, and Marta Kwiatkowska. 10051 Executive Summary – Quantitative and Qualitative Analysis of Network Protocols. In Quantitative and Qualitative Analysis of Network Protocols. Dagstuhl Seminar Proceedings, Volume 10051, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{jonsson_et_al:DagSemProc.10051.2,
  author =	{Jonsson, Bengt and Kreiker, J\"{o}rg and Kwiatkowska, Marta},
  title =	{{10051 Executive Summary – Quantitative and Qualitative Analysis of Network Protocols}},
  booktitle =	{Quantitative and Qualitative Analysis of Network Protocols},
  pages =	{1--1},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10051},
  editor =	{Bengt Jonsson and J\"{o}rg Kreiker and Marta Kwiatkowska},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10051.2},
  URN =		{urn:nbn:de:0030-drops-25165},
  doi =		{10.4230/DagSemProc.10051.2},
  annote =	{Keywords: Executive summary}
}
Document
DOI: 10.4230/DagSemRep.379
Probabilistic Methods in Verification and Planning (Dagstuhl Seminar 03201)

Authors: Craig Boutilier, Boudewijn Haverkort, Marta Kwiatkowska, and Moshe Y. Vardi

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Craig Boutilier, Boudewijn Haverkort, Marta Kwiatkowska, and Moshe Y. Vardi. Probabilistic Methods in Verification and Planning (Dagstuhl Seminar 03201). Dagstuhl Seminar Report 379, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2003)

Copy BibTex To Clipboard

@TechReport{boutilier_et_al:DagSemRep.379,
  author =	{Boutilier, Craig and Haverkort, Boudewijn and Kwiatkowska, Marta and Vardi, Moshe Y.},
  title =	{{Probabilistic Methods in Verification and Planning (Dagstuhl Seminar 03201)}},
  pages =	{1--8},
  ISSN =	{1619-0203},
  year =	{2003},
  type = 	{Dagstuhl Seminar Report},
  number =	{379},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.379},
  URN =		{urn:nbn:de:0030-drops-152590},
  doi =		{10.4230/DagSemRep.379},
}
Document
DOI: 10.4230/DagSemRep.273
Probabilistic Methods in Verification (Dagstuhl Seminar 00181)

Authors: Marta Kwiatkowska, Ulrich Herzog, Christoph Meinel, and Moshe Vardi

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Marta Kwiatkowska, Ulrich Herzog, Christoph Meinel, and Moshe Vardi. Probabilistic Methods in Verification (Dagstuhl Seminar 00181). Dagstuhl Seminar Report 273, pp. 1-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2000)

Copy BibTex To Clipboard

@TechReport{kwiatkowska_et_al:DagSemRep.273,
  author =	{Kwiatkowska, Marta and Herzog, Ulrich and Meinel, Christoph and Vardi, Moshe},
  title =	{{Probabilistic Methods in Verification (Dagstuhl Seminar 00181)}},
  pages =	{1--30},
  ISSN =	{1619-0203},
  year =	{2000},
  type = 	{Dagstuhl Seminar Report},
  number =	{273},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.273},
  URN =		{urn:nbn:de:0030-drops-151581},
  doi =		{10.4230/DagSemRep.273},
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact